XD1: Advanced Functional Programming in Lean
Lean is a modern, general-purpose programming language featuring advanced functional programming constructs such as pattern matching, recursion, immutable datastructures, type classes, dependent types and more. At the same time, Lean compiles to C++, featuring easy interopability with low-level libraries where necessary.
There are different angles that we could look at, depending on your and my interests:
Idea 1: Various Advanced Functional Programming Techniques
We can start with the functional programming, start with a toy arithmetic expression DSL and an interpreter. We could grow the language. We could learn to use of monads and monad transformers to represents effects, look into the difference between first-order and higher-order representations of syntax and their benefits and drawbacks, try out well-typed and well-scoped syntax. Maybe along the way something that fits your personal interest comes up?
Idea 2: More Pragmatic -- A Probabilistic Programming DSL
More pragmatically, we could implement a probabilistic programming language, for more ideas see also the probabilitsic programming topic in the seminar topics list.
Idea 3: More Theoretical -- Mathemtical Proofs with Integrals
Alternatively, more on the theoretical side, we could venturing further into the mechanization of mathmatical proofs using mathlib. Some time ago, Gouezel described a proof of the change of variables formula for integrals with mathlib, mechanized in Lean. One potential Goal of this project could be to figure out whether or how it was possible.